/*
 * To change this license header, choose License Headers in Project Properties.
 * To change this template file, choose Tools | Templates
 * and open the template in the editor.
 */
package tp2ia_partie2;


import java.io.BufferedOutputStream;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.PrintStream;
import java.util.LinkedHashSet;
import java.util.Set;
import tp2ia_partie2.objects.*;

/**
 *
 * @author hp
 */
public class TP2IA_partie2 {

    /**
     * @param args the command line arguments
     */
    public static void main(String[] args) throws FileNotFoundException {
        /*
         *     Création de l'énoncé
         */
        Litteral A = new Litteral("A");
        Litteral B = new Litteral("B");
        Litteral P = new Litteral("P");
        Litteral Q = new Litteral("Q");
        Litteral L = new Litteral("L");
        Litteral M = new Litteral("M");
        // c1
        Clause c1 = new RegleClause(P, Q);
        // c2
        Set<Litteral> faits2 = new LinkedHashSet<Litteral>();
        faits2.add(L);
        faits2.add(M);
        Clause c2 = new RegleClause(faits2, P);
        //c3
        Set<Litteral> faits3 = new LinkedHashSet<Litteral>();
        faits3.add(B);
        faits3.add(L);
        Clause c3 = new RegleClause(faits3, M);
        //c4
        Set<Litteral> faits4 = new LinkedHashSet<Litteral>();
        faits4.add(A);
        faits4.add(P);
        Clause c4 = new RegleClause(faits4, L);
        //c5
        Set<Litteral> faits5 = new LinkedHashSet<Litteral>();
        faits5.add(A);
        faits5.add(B);
        Clause c5 = new RegleClause(faits5, L);
        //c6
        Clause c6 = new DefiniesClause(A);
        //c7
        Clause c7 = new DefiniesClause(B);
        //c8 (but)
        Clause c8 = new ButClause(P);
        // creation de l'ensemble BK
        Set<Clause> KB = new LinkedHashSet<Clause>();
        KB.add(c1);
        KB.add(c2);
        KB.add(c3);
        KB.add(c4);
        KB.add(c5);
        KB.add(c6);
        KB.add(c7);

        //lancement de la resolution
        Resolution_1 resolutionEngine = new Resolution_1();
        boolean resolutionResult = resolutionEngine.plResolution(KB, c8);
        System.out.println("\n\n ____RESULTAT_____");
        System.out.println(resolutionResult ? "But prouvé" : "But non prouvé");

    }

}
